loc:Id, ds:x:Id fp Type, a:Id, T:Type, P:(State(ds)TProp).
@loc precondition for a(v:T):P State(ds) v  Realizer 

latex

Definitions	x:A. B(x), Prop, t  T, Realizer, @loc precondition for a(v:T):P State(ds) v, x. t(x), x(s)
Lemmas	decl-state wf, Knd wf, IdLnk wf, decl-type wf, unit wf, Id wf, fpf wf